(* Creme Caramel Compiler (Triple C) - Michele Caceffo - 2008 *)
(* 	Revision - Nataliia Bielova - 2011		      *)

open Exceptions;;
open Syntaxtree;;
open Declaration;;
open Intermediate;;

(** Contains all the functions to perform a small semantic analisys, which means only type checking :) 
    To do this has been introduced the "Semantic Type" which simplify the check
*)

(** Recovers the semantic type from an offset 
    @param t The element from which recover the type
    @return The semantic type of t
*)
let rec getType (t: element): sType = match t with
          Off(off, tp, _)    ->  tp
        | Reg(reg, tp)       ->  tp
        | _                  ->  raise (TYPE_ERROR "Type is not defined")

(* LDL: add a function useful to check the type correctness of pointer expressions *)
(** Checks the Semantic types of the pointer expressions
    @param ex The pointer expression to check
    @param The declarations table
    @param The procedures table.
           Note that this is not ever used in checkPexp but it is there for completeness,
           omogeneity wrt other check functions and for accommodationg future changes in the code.
           Nevertheless it is an option parameter, so it can also be None at the moment.
    @return The semantic type of ex
*)
let rec checkPexp (ex: pexp) (dect: dec_table) (proct: proc_table option) :sType = match ex with
    PVar(ide)   ->  let (_,_,t) = (getVarDeclaration4Semantics ide dect) in (getType t)
  | Ref(pexp)   ->  DPointer(checkPexp pexp dect proct)
  | Deref(pexp) -> ( 
                    match (checkPexp pexp dect proct) with			
			DPointer(pt) -> pt
		      | _ -> let err = "You are claiming to dereference a non pointer variable" in
			     raise (SEMANTIC_ERROR err)
                   )
(** Checks the Semantic types of the arithmetical expressions
    @param ex The arithmetical expression to check
    @param The declarations table
    @param The procedures table
    @return The semantic type of ex
*)
let rec checkAexp (ex: aexp) (dect: dec_table) (proct: proc_table) (tdtable: typedef_table) : sType = match ex with
          N(_)          ->  DInt
        | R(_)          ->  DFloat
	| Ox(_)         ->  DPointer(DWhatever) (* LDL: it represents a pointer to something undefined *)
	| PNull         ->  DPointer(DWhatever) (* LDL: it represents a pointer to something undefined *)
        | Var(i)        ->  let (_,_,t) = (getVarDeclaration4Semantics i dect) in (getType t)
	| P(Deref(pexp))->  (* LDL: it is only possible to have a dereferencing operator here at top-level.
			             In this case the expression is valid iff Deref(pexp) evaluates either
			              to Dpointer(DInt) or DPointer(DFloat) or DPointer(Whatever)
			              over static semantic.
			    *)
        	            checkPexp (Deref(pexp)) dect (Some(proct))
	| P(_)          -> let err = "You are claiming a pointer variable to be of arithmetic type, that is false" in
			   raise (SEMANTIC_ERROR err)
	| Rec(r)        -> (* LDL: add the static semantic part for records *)
	                   getSemanticOfRecord r dect tdtable
        | Vec(i,x)      ->  if ((checkAexp x dect proct tdtable) = DInt) then (
                                let (_,_,t) = (getVarDeclaration4Semantics i dect) in (getType t)
                            ) else (
                                raise (SEMANTIC_ERROR "Invalid Index")
                            )
        | Mat(i,x,y)    ->  if (((checkAexp x dect proct tdtable) = DInt) & ((checkAexp y dect proct tdtable) = DInt)) then (
                                let (_,_,t) = (getVarDeclaration4Semantics i dect) in (getType t)
                            ) else (
                                raise (SEMANTIC_ERROR "Invalid Index")
                            )
        (** For now are only allowed arithmetical operations between int and int or float and float, not mixed operations*)
        | Sum(ex1,ex2)  ->  (
                             let t1 = (checkAexp ex1 dect proct tdtable) and
                             t2 = (checkAexp ex2 dect proct tdtable) in
                             match (t1,t2) with
                                (DInt, DInt)                ->  DInt
                              | (DFloat, DFloat)            ->  DFloat
			      | (DPointer(_), DPointer(_))  ->  raise (SEMANTIC_ERROR "Pointer arithmetics is not allowed in CCC")
			      | (DRecord(i), DRecord(j)) when i = j -> raise (SEMANTIC_ERROR "Record arithmetics is not allowed in CCC")
                              | _                           ->  raise (SEMANTIC_ERROR "Different Types")
                            )
        | Sub(ex1,ex2)  ->  (
                             let t1 = (checkAexp ex1 dect proct tdtable) and
                             t2 = (checkAexp ex2 dect proct tdtable) in
                             match (t1,t2) with
                                (DInt, DInt)        ->  DInt
                              | (DFloat, DFloat)    ->  DFloat
			      | (DPointer(_), DPointer(_))  ->  raise (SEMANTIC_ERROR "Pointer arithmetics is not allowed in CCC")
			      | (DRecord(i), DRecord(j)) when i = j -> raise (SEMANTIC_ERROR "Record arithmetics is not allowed in CCC")
                              | _                   ->  raise (SEMANTIC_ERROR "Different Types")
                            )
        | Mul(ex1,ex2)  ->  (
                             let t1 = (checkAexp ex1 dect proct tdtable) and
                             t2 = (checkAexp ex2 dect proct tdtable) in
                             match (t1,t2) with
                                (DInt, DInt)        ->  DInt
                              | (DFloat, DFloat)    ->  DFloat
			      | (DPointer(_), DPointer(_))  ->  raise (SEMANTIC_ERROR "Pointer arithmetics is not allowed in CCC")
			      | (DRecord(i), DRecord(j)) when i = j -> raise (SEMANTIC_ERROR "Record arithmetics is not allowed in CCC")
                              | _                   ->  raise (SEMANTIC_ERROR "Different Types")
                            )
        | Div(ex1,ex2)  ->  (
                             let t1 = (checkAexp ex1 dect proct tdtable) and
                             t2 = (checkAexp ex2 dect proct tdtable) in
                             match (t1,t2) with
                                (DInt, DInt)        ->  DInt
                              | (DFloat, DFloat)    ->  DFloat
			      | (DPointer(_), DPointer(_))  ->  raise (SEMANTIC_ERROR "Pointer arithmetics is not allowed in CCC")
			      | (DRecord(i), DRecord(j)) when i = j -> raise (SEMANTIC_ERROR "Record arithmetics is not allowed in CCC")
                              | _                   ->  raise (SEMANTIC_ERROR "Different Types")
                            )
        | FCall(i,el)   ->  (
                             let pten = (Hashtbl.find proct i) in match pten with
                                Building(t, plist)              ->  (
                                                                     if (checkParTypes (List.rev plist) (List.rev el) dect proct tdtable)
                                                                     then (
                                                                         match t with
                                                                             SRet(Int)   -> DInt
                                                                           | SRet(Float) -> DFloat
									   (* LDL: add a pipe for the user defined type as return value *)
									   | SRet(UsrType(ut)) -> 
									     (*
									       match ut with
										   UsrRecord(r) ->
				                                                     (* LDL: add the static semantic part for records *)
										     (getSemanticOfRecord r tdtable)
									     *)
									     raise (SEMANTIC_ERROR "No user defined types as return values")
									   | Void        -> raise (SEMANTIC_ERROR "Void function")
                                                                     )
                                                                     else raise (SEMANTIC_ERROR "Different Parameters Types")
                                                                    )
                              | Subroutine(t,plist,_,_)   ->  (
                                                                     if (checkParTypes (List.rev plist) (List.rev el) dect proct tdtable)
                                                                     then (
                                                                         match t with
                                                                             SRet(Int)   -> DInt
                                                                           | SRet(Float) -> DFloat
									   (* LDL: add a pipe for the user defined type as return value *)
									   | SRet(UsrType(ut)) -> 
									     (*
									       match ut with
										   UsrRecord(r) ->
				                                                     (* LDL: add the static semantic part for records *)
										     (getSemanticOfRecord r tdtable)
									     *)
									     raise (SEMANTIC_ERROR "No user defined types as return values")
									   | Void        -> raise (SEMANTIC_ERROR "Void function")
                                                                     )
                                                                     else raise (SEMANTIC_ERROR "Different Parameters Types")
                                                                    )
                            )
(** Checks the semantic type of a list of parameters
    @param plist The list of formal parameters
    @param el The list of actual parameters
    @param dect The declarations table
    @param proct The procedures table
    @return True if the formal parameters types match with the actual parameters type, False otherwise
*)
(* LDL: we allow pointer parameter passing but for doing so it is necessary to introduce the param list concept (aexp list is no more enough) *)
(* LDL: we allow records to be passed to functons but we need the rec_tree in order to get their type in the case they were passed with pointers *)
and checkParTypes (plist: dec list) (el: actual list) (dect: dec_table) (proct: proc_table) (tdtable: typedef_table) = match (plist,el) with
          ([],[])                                          ->  true
        | ([x],[])                                         ->  true
        | (Dec(id,Basic(t))::ps,ParamAexp(e)::es)          ->  (
                                                                match t with
								    Int    ->  ((checkAexp e dect proct tdtable) = DInt) & checkParTypes ps es dect proct tdtable
								  | Float  ->  ((checkAexp e dect proct tdtable) = DFloat) & checkParTypes ps es dect proct tdtable
								  (* LDL: add a pipe for the user defined type as return value *)
								  | UsrType(ut) -> (* LDL: add a pipe for the user defined type as return value *)
								    let record_stype = match ut with
									UsrRecord(r) -> (getSemanticOfRecord r dect tdtable)
								    in
								    ((checkAexp e dect proct tdtable) = record_stype) &
								      checkParTypes ps es dect proct tdtable
                                                               )
	| (Dec(id,Pointer(gtype))::ps,ParamAexp(e)::es)    ->  
	  let ls = (checkAexp e dect proct tdtable) and rs = (getSemanticGtype (Pointer(gtype)) dect tdtable) in
	  (
	    match rs with 
		DPointer(_) when ls = DPointer(DWhatever) -> true & checkParTypes ps es dect proct tdtable
	      | _ -> (ls = rs) & checkParTypes ps es dect proct tdtable
	  )
	| (Dec(id,Pointer(gtype))::ps,ParamPexp(pexp)::es) ->  
	            ((checkPexp pexp dect (Some(proct))) = (getSemanticGtype (Pointer(gtype)) dect tdtable)) & checkParTypes ps es dect proct tdtable
        | _                                                -> raise (SEMANTIC_ERROR "Wrong Parameters Number");

(** Checks the semantic type of boolean operations (compare is only allowed between int and int or float and float, 
    not mixed operations)
    @param b The boolean operation to check
    @param dect The declarations table
    @param proct The procedures table
    @return The sematic type of b
*)
(* LDL: forbid to compare pointers but allow records *)
and checkBool (b: bexp) (dect: dec_table) (proct: proc_table) (tdtable: typedef_table) = match b with
          B(b)          ->  DBool
        | Equ(ex1,ex2)  ->  (
                             let t1 = (checkAexp ex1 dect proct tdtable) and
                             t2 = (checkAexp ex2 dect proct tdtable) in
                             match (t1,t2) with
                                (DInt, DInt)               ->  DBool
                              | (DFloat, DFloat)           ->  DBool
			      | (DPointer(_), DPointer(_)) ->  raise (SEMANTIC_ERROR "Equ undefined for pointers") (* LDL: p1 = p2 : not allowed *)
			      | (DRecord(i), DRecord(j)) when i=j -> DBool
                              | _                          ->  raise (SEMANTIC_ERROR "Different Types")
                            )
        | LE(ex1,ex2)   ->  (
                             let t1 = (checkAexp ex1 dect proct tdtable) and
                             t2 = (checkAexp ex2 dect proct tdtable) in
                             match (t1,t2) with
                                (DInt, DInt)               ->  DBool
                              | (DFloat, DFloat)           ->  DBool
			      | (DPointer(_), DPointer(_)) ->  raise (SEMANTIC_ERROR "LE undefined for pointers") (* LDL: p1 <= p2 : not allowed *)
			      | (DRecord(i), DRecord(j)) when i=j -> DBool
                              | _                          ->  raise (SEMANTIC_ERROR "Different Types")
                            )
        | LT(ex1,ex2)   ->  (
                             let t1 = (checkAexp ex1 dect proct tdtable) and
                             t2 = (checkAexp ex2 dect proct tdtable) in
                             match (t1,t2) with
                                (DInt, DInt)               ->  DBool
                              | (DFloat, DFloat)           ->  DBool
			      | (DPointer(_), DPointer(_)) ->  raise (SEMANTIC_ERROR "LT undefined for pointers") (* LDL: p1 < p2 : not allowed *)
			      | (DRecord(i), DRecord(j)) when i=j -> DBool
                              | _                          ->  raise (SEMANTIC_ERROR "Different Types")
                            )
        | Not(bx)       ->  if ((checkBool bx dect proct tdtable) = DBool) then DBool else raise (SEMANTIC_ERROR "Different Types")
        | And(bx1,bx2)  ->  (
                             let t1 = (checkBool bx1 dect proct tdtable) and
                             t2 = (checkBool bx2 dect proct tdtable) in
                             match (t1,t2) with
                                (DBool, DBool)      ->  DBool
                              | _                   ->  raise (SEMANTIC_ERROR "Different Types")
                            )
        | Or(bx1,bx2)   ->  (
                             let t1 = (checkBool bx1 dect proct tdtable) and
                             t2 = (checkBool bx2 dect proct tdtable) in
                             match (t1,t2) with
                                (DBool, DBool)      ->  DBool
                              | _                   ->  raise (SEMANTIC_ERROR "Different Types")
                            )

(** Checks the semantic type of left expression
    @param l The left expression to check
    @param dect The declarations table
    @return The semantic type of l
*)
let checkLexp (l: lexp) (dect: dec_table) proct (tdtable: typedef_table) = match l with
          LVar(i)       ->  let (_,_,t) = (getVarDeclaration4Semantics i dect) in (getType t)
        | LPexpr(pexpr) ->  (* LDL: we want the pointer to be evaluated to a pointer variable *)
	                    checkPexp pexpr dect (Some(proct))
	| LRec(r)       ->  (getSemanticOfRecord r dect tdtable)
        | LVec(i,x)     ->  if ((checkAexp x dect proct tdtable) = DInt) then (
                                let (_,_,t) = (getVarDeclaration4Semantics i dect) in (getType t)
                            ) else (
                                raise (SEMANTIC_ERROR "Invalid Index")
                            )
        | LMat(i,x,y)    ->  if (((checkAexp x dect proct tdtable) = DInt) & ((checkAexp y dect proct tdtable) = DInt)) then (
                                let (_,_,t) = (getVarDeclaration4Semantics i dect) in (getType t)
                            ) else (
                                raise (SEMANTIC_ERROR "Invalid Index")
                            )

(** Checks the semantic type of commands
    @param c The command to check
    @param dect The declarations table
    @return True of the command is well formed (type checking is good), False otherwise
*)
let rec cmdsemantic (c: cmd) (dect: dec_table) proct (tdtable: typedef_table) = match c with
          Ass(l,r)      ->  (* LDL: modify this wrt DWhatever introduction. DWhatever is used only
			            in the case of direct pointer specification (like px = 0x(12)).
			    *)
	                    let lv = (checkLexp l dect proct tdtable) and rv = (checkAexp r dect proct tdtable) in
			    (
			      match lv with				  
				  DPointer(_) when rv = (DPointer(DWhatever)) -> true
				| _ -> lv = rv
			    )
        | PAss(l,r)     ->  (* LDL: check the correctness of the pointer assignment command*)	                    
			    (* LDL: modify this wrt DWhatever introduction. DWhatever is used only
			            in the case of direct pointer specification (like px = 0x(12)).
			    *)
	                    let lv = (checkLexp l dect proct tdtable) and rv = (checkPexp r dect (Some(proct))) in
			    (
			      match lv with
				  DPointer(_) when rv = (DPointer(DWhatever)) -> true
				| _ -> lv = rv
			    )
        | Blk(cl)       ->  (
                             match cl with
                                []      ->  true
                              | x::xs   ->  (cmdsemantic x dect proct tdtable) & (cmdsemantic (Blk(xs)) dect proct tdtable)
                            )
        | Ite(b,c1,c2)  ->  ((checkBool b dect proct tdtable) = DBool) & (cmdsemantic c1 dect proct tdtable) & (cmdsemantic c2 dect proct tdtable)
        | While(b,c)    ->  ((checkBool b dect proct tdtable) = DBool) & (cmdsemantic c dect proct tdtable)
        | Repeat(c,b)   ->  ((checkBool b dect proct tdtable) = DBool) & (cmdsemantic c dect proct tdtable)
        | For(i,s,f,c)  ->  let it = (checkAexp (Var(i)) dect proct tdtable) in
                            (it = (checkAexp s dect proct tdtable)) & 
                            (it = (checkAexp f dect proct tdtable)) & 
                            (it = DInt) &
                            (cmdsemantic c dect proct tdtable)
        | Write(e)      ->  (try (let _ = (checkAexp e dect proct tdtable)  in true ) 
			    with (SEMANTIC_ERROR _) -> false )
				
        | PCall(i,pl)   ->  (
                             let pten = (Hashtbl.find proct i) in match pten with
                                Building(t, plist)              ->  (
                                                                     if (checkParTypes (List.rev plist) (List.rev pl) dect proct tdtable)
                                                                     then true
                                                                     else raise (SEMANTIC_ERROR "Different Parameters Types")
                                                                    )
                              | Subroutine(t,plist,ldtable,_)   ->  (
                                                                     if (checkParTypes (List.rev plist) (List.rev pl) dect proct tdtable)
                                                                     then true
                                                                     else raise (SEMANTIC_ERROR "Different Parameters Types")
                                                                    )
                            )
